<html>
<head><meta charset="utf-8"><title>intersection type · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html">intersection type</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="164005953"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164005953" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164005953">(Apr 23 2019 at 16:31)</a>:</h4>
<blockquote>
<p>the idea is "some value is both T1 and T2 simultaneously"</p>
</blockquote>
<p>what property does it have that isn't satisfied by a product? i.e. if <code>typeof(x) = T1 &amp;&amp; T2</code> and <code>typeof( (t1, t2) ) = T1 x T2</code>, what would we expect to be true of <code>x</code> that we don't get by doing something on <code>t1</code> or <code>t2</code> separately?</p>



<a name="164006073"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006073" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006073">(Apr 23 2019 at 16:32)</a>:</h4>
<p>Maybe I am confused -- a product <code>(T1, T2)</code> is the combination of a T1 and T2 value (and you can project out those independent things). But importantly <em>any</em> T1 and T2 value can be combined.</p>



<a name="164006075"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006075" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006075">(Apr 23 2019 at 16:32)</a>:</h4>
<p>or maybe another way to ask my question is: why should <code>dyn (Foo + Bar)</code> be modelled by <code>dyn Foo &amp;&amp; dyn Bar</code>, where <code>&amp;&amp;</code> has the obvious trait bound criteria, rather than <code>dyn (Foo + Bar)</code> directly having the obvious bound criteria?</p>



<a name="164006084"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006084" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006084">(Apr 23 2019 at 16:32)</a>:</h4>
<p>An intersection is a <em>single</em> value that is both</p>



<a name="164006113"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006113" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006113">(Apr 23 2019 at 16:33)</a>:</h4>
<p>i.e. <code>dyn (trait bound) : trait bound.</code></p>



<a name="164006148"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006148" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006148">(Apr 23 2019 at 16:33)</a>:</h4>
<p>that is, <code>dyn</code> is parameterised by a bound, rather than by a list of traits</p>



<a name="164006271"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006271" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006271">(Apr 23 2019 at 16:35)</a>:</h4>
<blockquote>
<p>An intersection is a single value that is both</p>
</blockquote>
<p>ah, so an intersection type here is a product without projections</p>



<a name="164006273"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006273" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006273">(Apr 23 2019 at 16:35)</a>:</h4>
<p>it's not clear that what I am thinking makes sense, but my reasoning was that I wanted to avoid quantifying over something that is not types. That said, I think that it may work out fine to support <code>dyn Bound1 + Bound2</code> directly, and to lower that in chalk's "program clause" callback to</p>
<ul>
<li><code>dyn (Bound1 + Bound2): Bound1</code></li>
<li><code>dyn (Bound1 + Bound2): Bound2</code></li>
</ul>



<a name="164006398"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006398" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006398">(Apr 23 2019 at 16:36)</a>:</h4>
<p>I think it's very possible it'll be necessary to parameterise over bounds at some point in the future regardless (e.g. any of the various "constraint kinds" proposals)</p>



<a name="164006412"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006412" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006412">(Apr 23 2019 at 16:36)</a>:</h4>
<blockquote>
<p>that is, dyn is parameterised by a bound, rather than by a list of traits</p>
</blockquote>
<p>To that point, the way I would model <code>dyn Trait</code> in Haskell is:</p>
<div class="codehilite"><pre><span></span><span class="kr">data</span> <span class="kt">Dyn</span> <span class="p">(</span><span class="n">c</span> <span class="ow">::</span> <span class="kt">Type</span> <span class="ow">-&gt;</span> <span class="kt">Constraint</span><span class="p">)</span> <span class="ow">=</span> <span class="n">forall</span> <span class="p">(</span><span class="n">t</span> <span class="ow">::</span> <span class="kt">Type</span><span class="p">)</span><span class="o">.</span> <span class="p">(</span><span class="n">c</span> <span class="n">t</span><span class="p">)</span> <span class="ow">=&gt;</span> <span class="kt">D</span> <span class="n">t</span>
</pre></div>



<a name="164006447"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006447" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006447">(Apr 23 2019 at 16:37)</a>:</h4>
<blockquote>
<p>I think it's very possible it'll be necessary to parameterise over bounds at some point in the future regardless (e.g. any of the various "constraint kinds" proposals)</p>
</blockquote>
<p>plausible, but I would rather not</p>



<a name="164006462"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006462" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006462">(Apr 23 2019 at 16:37)</a>:</h4>
<p>well, that's strong</p>



<a name="164006488"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006488" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006488">(Apr 23 2019 at 16:37)</a>:</h4>
<p>but I would rather not go there if we don't have to</p>



<a name="164006495"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006495" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006495">(Apr 23 2019 at 16:37)</a>:</h4>
<p>that said, I don't think we have to quantify over predicates in any case</p>



<a name="164006545"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006545" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006545">(Apr 23 2019 at 16:38)</a>:</h4>
<p>in either scheme</p>



<a name="164006554"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006554" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006554">(Apr 23 2019 at 16:38)</a>:</h4>
<p>as this logic would be "internal" to the callback, and implemented in Rust</p>



<a name="164006559"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006559" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006559">(Apr 23 2019 at 16:38)</a>:</h4>
<blockquote>
<p>ah, so an intersection type here is a product without projections</p>
</blockquote>
<p>sorry, this is a confusing way of putting it — I essentially mean that we have the following introduction rule (and the obvious formation rule):<br>
<code>a: A, b: B ==&gt; a&amp;b : A &amp;&amp; B</code><br>
but <em>no</em> elimination (or computation) rules</p>



<a name="164006569"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006569" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006569">(Apr 23 2019 at 16:38)</a>:</h4>
<blockquote>
<p>but I would rather not go there if we don't have to</p>
</blockquote>
<p>(though it's worth nothing that Lambda Calculus generally permits one to quantify over predicates)</p>



<a name="164006592"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006592" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006592">(Apr 23 2019 at 16:39)</a>:</h4>
<blockquote>
<p>but no elimination (or computation) rules</p>
</blockquote>
<p>which is equivalent to a product type without projections</p>



<a name="164006710"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006710" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006710">(Apr 23 2019 at 16:40)</a>:</h4>
<blockquote>
<p>but I would rather not go there if we don't have to</p>
</blockquote>
<p>Having <code>dyn Self::MyBound</code> work is definitely something that I'm interested in exploring as part of <code>-XConstraintKinds</code> in Rust (associated traits, trait generics, ...)</p>



<a name="164006713"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006713" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006713">(Apr 23 2019 at 16:40)</a>:</h4>
<blockquote>
<p>but I would rather not go there if we don't have to</p>
</blockquote>
<p>it's fairly tangential anyway<br>
I just think that parameterisation over bounds is going to lead to a simpler (conceptual) model</p>



<a name="164006764"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164006764" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164006764">(Apr 23 2019 at 16:41)</a>:</h4>
<p>(of course, I'm saying this without having tried to implement anything, so there are a lot of handfuls of salt to be taken here <span aria-label="grinning face with smiling eyes" class="emoji emoji-1f601" role="img" title="grinning face with smiling eyes">:grinning_face_with_smiling_eyes:</span>)</p>



<a name="164007305"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164007305" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164007305">(Apr 23 2019 at 16:48)</a>:</h4>
<p><a href="/user_uploads/4715/vFHb0RGoBomKWmkTK0q_GkES/pasted_image.png" target="_blank" title="pasted_image.png">pasted image</a></p>
<div class="message_inline_image"><a href="/user_uploads/4715/vFHb0RGoBomKWmkTK0q_GkES/pasted_image.png" target="_blank" title="pasted image"><img src="/user_uploads/4715/vFHb0RGoBomKWmkTK0q_GkES/pasted_image.png"></a></div>



<a name="164007315"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164007315" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164007315">(Apr 23 2019 at 16:48)</a>:</h4>
<p>(I think this is the definition of an intersection type)</p>



<a name="164007424"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164007424" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164007424">(Apr 23 2019 at 16:50)</a>:</h4>
<p>(namely, if an <code>a: A</code> satisfies some property <code>p</code> and <code>b: B</code>satisfies some property <code>q</code>, then there exists some object <code>f(a, b): A &amp; B</code> such that <code>f(a, b)</code> satisfies both <code>p</code> and <code>q</code>)</p>



<a name="164007569"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164007569" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164007569">(Apr 23 2019 at 16:53)</a>:</h4>
<blockquote>
<p>I just think that parameterisation over bounds is going to lead to a simpler (conceptual) model</p>
</blockquote>
<p>having thought it over, I think I agree</p>



<a name="164007937"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164007937" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164007937">(Apr 23 2019 at 16:57)</a>:</h4>
<p><span class="user-mention" data-user-id="121053">@varkor</span> that looks similar to the diagram for a product; i.e. set <code>p, p', q', q = id</code></p>



<a name="164008107"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164008107" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164008107">(Apr 23 2019 at 16:59)</a>:</h4>
<p><span class="user-mention" data-user-id="126931">@centril</span>: if you replace the two <code>Ω</code>s by <code>A</code> and <code>B</code>, then you get a product — but here <code>Ω</code> is an "object of truth values" (in Rust's case, this would just be <code>bool</code>)</p>



<a name="164008152"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164008152" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164008152">(Apr 23 2019 at 16:59)</a>:</h4>
<p>the difference being that with an intersection type, you want to preserve the values of propositions, but you don't want to be able to project</p>



<a name="164008223"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164008223" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164008223">(Apr 23 2019 at 17:00)</a>:</h4>
<p>(<code>Ω</code> here is known as a subobject classifier)</p>



<a name="164008233"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164008233" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164008233">(Apr 23 2019 at 17:00)</a>:</h4>
<p>(this is really just a modification of the definition of a pullback over the subobject classifier in a topos)</p>



<a name="164008268"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164008268" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164008268">(Apr 23 2019 at 17:00)</a>:</h4>
<p><span class="user-mention" data-user-id="121053">@varkor</span> so you are using truncation?</p>



<a name="164008378"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164008378" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164008378">(Apr 23 2019 at 17:02)</a>:</h4>
<p>truncations aren't really relevant here, because there's no identity type / higher dimensionality</p>



<a name="164008430"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164008430" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164008430">(Apr 23 2019 at 17:03)</a>:</h4>
<p><em>edit: I'll rephrase</em></p>



<a name="164008463"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164008463" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164008463">(Apr 23 2019 at 17:03)</a>:</h4>
<p><span class="user-mention" data-user-id="121053">@varkor</span> here's where my category theory-fuu falls short ;)</p>



<a name="164008884"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164008884" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164008884">(Apr 23 2019 at 17:08)</a>:</h4>
<blockquote>
<p>you want to preserve the values of propositions, but you don't want to be able to project</p>
</blockquote>
<p><span class="user-mention" data-user-id="121053">@varkor</span> but this reminded me of <code>Type</code> &amp; <code>Prop</code> ; i.e. we want to erase the witness and have proof irrelevance</p>



<a name="164008982"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164008982" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164008982">(Apr 23 2019 at 17:09)</a>:</h4>
<p>I'll explain a bit more intuitively</p>



<a name="164008984"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164008984" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164008984">(Apr 23 2019 at 17:09)</a>:</h4>
<p><a href="/user_uploads/4715/uuQY9gB0SegzKy7l7toqi7Np/pasted_image.png" target="_blank" title="pasted_image.png">pasted image</a></p>
<div class="message_inline_image"><a href="/user_uploads/4715/uuQY9gB0SegzKy7l7toqi7Np/pasted_image.png" target="_blank" title="pasted image"><img src="/user_uploads/4715/uuQY9gB0SegzKy7l7toqi7Np/pasted_image.png"></a></div>



<a name="164008991"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164008991" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164008991">(Apr 23 2019 at 17:09)</a>:</h4>
<p>this is a typical product type (in context Gamma)</p>



<a name="164009057"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009057" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009057">(Apr 23 2019 at 17:10)</a>:</h4>
<p>sure</p>



<a name="164009062"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009062" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009062">(Apr 23 2019 at 17:10)</a>:</h4>
<p>it's trivially the same as this diagram:</p>



<a name="164009064"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009064" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009064">(Apr 23 2019 at 17:10)</a>:</h4>
<p><a href="/user_uploads/4715/2a6gxkWla-pTiX0Hpug_myC0/pasted_image.png" target="_blank" title="pasted_image.png">pasted image</a></p>
<div class="message_inline_image"><a href="/user_uploads/4715/2a6gxkWla-pTiX0Hpug_myC0/pasted_image.png" target="_blank" title="pasted image"><img src="/user_uploads/4715/2a6gxkWla-pTiX0Hpug_myC0/pasted_image.png"></a></div>



<a name="164009069"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009069" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009069">(Apr 23 2019 at 17:10)</a>:</h4>
<p>because you can take A = A' and B = B'</p>



<a name="164009111"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009111" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009111">(Apr 23 2019 at 17:11)</a>:</h4>
<p>however, if we don't let A' and B' be arbitrary, this is no longer as general as a product type, because you have "projections" only to the specified types A' and B'</p>



<a name="164009120"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009120" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009120">(Apr 23 2019 at 17:11)</a>:</h4>
<p>in particular, if we take A' = B' = Bool, then we get this</p>



<a name="164009156"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009156" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009156">(Apr 23 2019 at 17:11)</a>:</h4>
<p><a href="/user_uploads/4715/bQTbFGMbQ3AB7vaCGMmtBp2N/pasted_image.png" target="_blank" title="pasted_image.png">pasted image</a></p>
<div class="message_inline_image"><a href="/user_uploads/4715/bQTbFGMbQ3AB7vaCGMmtBp2N/pasted_image.png" target="_blank" title="pasted image"><img src="/user_uploads/4715/bQTbFGMbQ3AB7vaCGMmtBp2N/pasted_image.png"></a></div>



<a name="164009231"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009231" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009231">(Apr 23 2019 at 17:12)</a>:</h4>
<p>(well, the A x B in the middle should be something else, e.g. <code>A &amp; B</code>)</p>



<a name="164009237"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009237" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009237">(Apr 23 2019 at 17:12)</a>:</h4>
<p>here, our "projections" are only permitted to <code>bool</code></p>



<a name="164009250"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009250" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009250">(Apr 23 2019 at 17:12)</a>:</h4>
<p>i.e. the projections are just functions to <code>bool</code>, or propositions</p>



<a name="164009295"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009295" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009295">(Apr 23 2019 at 17:13)</a>:</h4>
<p>so this means that the type <code>A &amp; B</code> satisfies the same propositions as <code>A</code> and <code>B</code> separately, but you can't project</p>



<a name="164009306"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009306" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009306">(Apr 23 2019 at 17:13)</a>:</h4>
<p>(we can obviously convert any product type into an intersection type)</p>



<a name="164009373"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009373" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009373">(Apr 23 2019 at 17:14)</a>:</h4>
<p>(the type <code>bool</code> is known as a subobject classifier in a topos)</p>



<a name="164009383"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009383" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009383">(Apr 23 2019 at 17:14)</a>:</h4>
<p>(but that's not important :) )</p>



<a name="164009471"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009471" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009471">(Apr 23 2019 at 17:15)</a>:</h4>
<p>(it looks a little like a pullback type, but it's not as general)</p>



<a name="164009498"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009498" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009498">(Apr 23 2019 at 17:15)</a>:</h4>
<p>so now we can define an "intersection type" in any category</p>



<a name="164009641"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009641" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009641">(Apr 23 2019 at 17:17)</a>:</h4>
<p><span class="user-mention" data-user-id="121053">@varkor</span> so we can get an intersection type by taking the usual product type but leave out the projections?</p>



<a name="164009799"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009799" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009799">(Apr 23 2019 at 17:19)</a>:</h4>
<p>you need these extra functions to <code>bool</code>, I think — otherwise the type isn't really an "intersection"</p>



<a name="164009812"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164009812" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164009812">(Apr 23 2019 at 17:19)</a>:</h4>
<p>it's just some type that's guaranteed to exist</p>



<a name="164010642"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/intersection%20type/near/164010642" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> varkor <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/intersection.20type.html#164010642">(Apr 23 2019 at 17:28)</a>:</h4>
<p>(the confusing thing about the nomenclature here is that this definition does not give the usual notion of intersection of sets)</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>